modal logic

An extension of propositional calculus with operators that

express various "modes" of truth. Examples of modes are:

necessarily A, possibly A, probably A, it has always been true

that A, it is permissible that A, it is believed that A.

"It is necessarily true that A" means that things being as

they are, A must be true, e.g.

"It is necessarily true that x=x" is TRUE

while

"It is necessarily true that x=y" is FALSE

even though "x=y" might be TRUE.

Adding modal operators [F] and [P], meaning, respectively,

henceforth and hitherto leads to a "temporal logic".

Flavours of modal logics include: Propositional DynamicLogic (PDL), Propositional Linear Temporal Logic (PLTL),

Linear Temporal Logic (LTL), Computational Tree Logic

(CTL), Hennessy-Milner Logic, S1-S5, T.

C.I. Lewis, "A Survey of Symbolic Logic", 1918, initiated the

modern analysis of modality. He developed the logical systems

S1-S5. JCC McKinsey used algebraic methods (Booleanalgebras with operators) to prove the decidability of Lewis'

S2 and S4 in 1941. Saul Kripke developed the relationalsemantics for modal logics (1959, 1963). Vaughan Pratt

introduced dynamic logic in 1976. Amir Pnuelli proposed the

use of temporal logic to formalise the behaviour of

continually operating concurrent programs in 1977.

[Robert Goldblatt, "Logics of Time and Computation", CSLI

Lecture Notes No. 7, Centre for the Study of Language and

Information, Stanford University, Second Edition, 1992,

(distributed by University of Chicago Press)].

[Robert Goldblatt, "Mathematics of Modality", CSLI Lecture

Notes No. 43, Centre for the Study of Language and

Information, Stanford University, 1993, (distributed by

University of Chicago Press)].

[G.E. Hughes and M.J. Cresswell, "An Introduction to Modal

Logic", Methuen, 1968].

[E.J. Lemmon (with Dana Scott), "An Introduction to Modal

Logic", American Philosophical Quarterly Monograpph Series,

no. 11 (ed. by Krister Segerberg), Basil Blackwell, Oxford,

1977].

(1995-02-15)